ds:x:Id fp Type, knd:Knd, T:Type, l:IdLnk, dt:x:Id fp Type,
g:(tg:Id(State(ds)T(DeclaredType(dt;tg) List))) List.
sends knd(v:T) on l:tagged(g,State(ds),v):dt  Realizer 

latex

Definitions	x:A. B(x), t  T, Realizer, sends knd(v:T) on l:tagged(g,State(ds),v):dt, Prop, x. t(x), x(s)
Lemmas	decl-state wf, decl-type wf, IdLnk wf, Knd wf, unit wf, Id wf, fpf wf